let L1, L2 be non empty up-complete Poset; :: thesis: for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds
( x is compact iff f . x is compact )
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies for x being Element of L1 holds
( x is compact iff f . x is compact ) )
assume A1: f is isomorphic ; :: thesis: for x being Element of L1 holds
( x is compact iff f . x is compact )
let x be Element of L1; :: thesis: ( x is compact iff f . x is compact )
thus ( x is compact implies f . x is compact ) :: thesis: ( f . x is compact implies x is compact )
proof
assume x is compact ; :: thesis: f . x is compact
then x << x by WAYBEL_3:def 2;
then f . x << f . x by A1, Th27;
hence f . x is compact by WAYBEL_3:def 2; :: thesis: verum
end;
thus ( f . x is compact implies x is compact ) :: thesis: verum
proof
assume f . x is compact ; :: thesis: x is compact
then f . x << f . x by WAYBEL_3:def 2;
then x << x by A1, Th27;
hence x is compact by WAYBEL_3:def 2; :: thesis: verum
end;