let L1, L2 be RelStr ; :: thesis: for f being Function of L1,L2 st f is isomorphic holds

( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

let f be Function of L1,L2; :: thesis: ( f is isomorphic implies ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) ) )

assume A1: f is isomorphic ; :: thesis: ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

( the carrier of L1 = {} iff the carrier of L2 = {} )

( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

let f be Function of L1,L2; :: thesis: ( f is isomorphic implies ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) ) )

assume A1: f is isomorphic ; :: thesis: ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

( the carrier of L1 = {} iff the carrier of L2 = {} )

proof

then L2 is empty ;

then L1 is empty by A1, WAYBEL_0:def 38;

hence the carrier of L1 = {} ; :: thesis: verum

end;

hence
( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
; :: thesis: verumhereby :: thesis: ( the carrier of L2 = {} implies the carrier of L1 = {} )

assume
the carrier of L2 = {}
; :: thesis: the carrier of L1 = {} assume
the carrier of L1 = {}
; :: thesis: the carrier of L2 = {}

then L1 is empty ;

then L2 is empty by A1, WAYBEL_0:def 38;

hence the carrier of L2 = {} ; :: thesis: verum

end;then L1 is empty ;

then L2 is empty by A1, WAYBEL_0:def 38;

hence the carrier of L2 = {} ; :: thesis: verum

then L2 is empty ;

then L1 is empty by A1, WAYBEL_0:def 38;

hence the carrier of L1 = {} ; :: thesis: verum